; <lemma>
;  <title>ch7_conc.26</title>
;  <origin>ch7_conc | conc_2 | Writer_41/inv16/INV</origin>
(benchmark ch7_conc_26
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="n" type="INTEGER"/>
;    <variable name="x" type="INTEGER"/>
;    <variable name="y" type="INTEGER"/>
;  </typenv>
  :extrafuns ((n Int)(x Int)(y Int))
  :extramacros (
		 (Nat1 (lambda (?i Int) . (<= 1 ?i)))
		 (in (lambda (?x1 't1) (?p ('t1 boolean)) . (?p ?x1)))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 )
; <hypothesis needed="true">n : NATURAL1</hypothesis>
  :assumption (in n Nat1)
; <hypothesis needed="true">1 .. n = 1 .. n+1</hypothesis>
  :assumption (= (range 1 n) (range 1 (+ 1 n)))
; <goal needed="false">x = y</goal>
  :formula
  (not
      (= x y)
    )
)
; </lemma>
